R. Kashima, Y. Kato; 2022; "Semantical Cut-Elimination for the Provability Logic of True Arithmetic"
https://arxiv.org/abs/2309.05948
Ref
鹿島 亮，Yutaka Kato
$ \sf GLS（様相論理GLS）という様相論理GLの拡張についてのカット除去定理（意味論的カット除去定理）について
$ \sf GLに公理$ \Box A \to Aを追加した体系
remark
この公理は$ T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner) \implies T \vdash \varphiと解釈される．
算術の標準モデルに翻訳可能という意味で完全
G. Boolos; "The Logic of Provability"
Robert M. Solovay; 1976; "Provability Interpretation of Modal Logic"と$ \sf G'と呼ばれている
非正規様相論理としては最も知られているモノらしい
A. Chagrov, M. Zakharyaschev; "Modal Logic"では$ \sf Sと呼ばれている
H. Kushida; "A proof theory for the logic of provability in true arithmetic"で証明論的な研究がなされている